<html>
<head><meta charset="utf-8"><title>dafny · t-compiler/wg-polonius · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/index.html">t-compiler/wg-polonius</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html">dafny</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="202299600"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/202299600" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andrea Lattuada <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#202299600">(Jun 29 2020 at 12:01)</a>:</h4>
<p>Hi folks, I’m a research intern at VMware (PhD student at ETH Zürich, where I worked with Frank). I’m currently experimenting with “duct-taping” polonius to the <code>dafny</code> programming language (if you’re unfamiliar, it’s a verification+imperative language from MSR; its imperative part is similar to c#). I’m working with some of the authors of the IronClad/IronFleet papers on a new verification project attempting to extend the usability of the tools to large code-bases. As others have realised, we think linear types are an important step forward (as they alleviate some of the compelxity of reasoning); we have basic (experimental) linear type support built to dafny, and my plan is to extend this support to more of the idioms allowed in rust (thanks to borrowing). Because polonius it’s nicely factored out as a datalog engine, it seems like a prime candidate to attempt the integration.<br>
I realise this may be equal parts(?) interesting and terrifying for peeps in the WG :) The good news is that you’d have another “user”, who’s also happy to contribute diagnostic/other fixes; the “bad" news is that we’re somehow misusing the analysis for a different language.</p>



<a name="202305968"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/202305968" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#202305968">(Jun 29 2020 at 13:07)</a>:</h4>
<p>interesting :)</p>



<a name="202306038"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/202306038" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#202306038">(Jun 29 2020 at 13:07)</a>:</h4>
<p>dafny seemed nice, even though I also had my eye on why3 and whiley</p>



<a name="202306761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/202306761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#202306761">(Jun 29 2020 at 13:14)</a>:</h4>
<p>but I need to mention that the analyses in polonius are not finalized yet, it's still a work in progress. maybe focusing on reusing the datalog rules and concepts, more so than the complete implementation itself (which can and will change), could be a "less unstable" basis for your own work</p>



<a name="202323762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/202323762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andrea Lattuada <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#202323762">(Jun 29 2020 at 15:09)</a>:</h4>
<p>Yup! We like dafny for a few reasons, one being that we think it’s more natural for engineers who don’t have a verification background (and, for the same reason, we’ve also been looking at Prusti, the Viper-based verifier for Rust developed at ETH). Thanks for the note. I’m aware that Polonius isn’t finalised, and that’s totally fine by me/us; the final language it would target in our project isn’t well defined yet either. If things diverge, that’s totally okay! (although I have a feeling that some of the things that are still WIP in polonius are for features we don’t need yet, like the interaction with traits). I’ll try to keep a divergent branch orderly, so we can still cherry-pick if there’s anything of use to the “real” polonius. Other reasons I’m experimenting with Polonius: (i) I can write some rust and see what the generated facts look like and (ii)  datafrog is neat and I’m already a bit familiar.</p>



<a name="202323935"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/202323935" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andrea Lattuada <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#202323935">(Jun 29 2020 at 15:10)</a>:</h4>
<p>(Also, please let me know if this is out-of-scope for the wg-polonius stream and I’ll move the communication elsewhere.)</p>



<a name="203017797"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203017797" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203017797">(Jul 06 2020 at 17:28)</a>:</h4>
<p>This sounds super cool! I've been looking at doing stuff with Dafny as well; I'm a PhD student for my day job where I work on string solvers for SMT and applying them for verification</p>



<a name="203018362"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203018362" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203018362">(Jul 06 2020 at 17:34)</a>:</h4>
<p>I would also suggest perhaps using something like Soufflé if you can rather than datafrog; as nice as it is, I believe Soufflé is much more mature</p>



<a name="203022538"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203022538" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Eh2406 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203022538">(Jul 06 2020 at 18:11)</a>:</h4>
<p>Off topic, but what is a <code>string solvers</code>?</p>



<a name="203022900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203022900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Eh2406 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203022900">(Jul 06 2020 at 18:15)</a>:</h4>
<p>I know some about SAT and have some idea about how SMT is an extension, but don't know that term.</p>



<a name="203024825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203024825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Eh2406 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203024825">(Jul 06 2020 at 18:33)</a>:</h4>
<p>Some googling later, it extends the available data types to include  <code>string</code>. That makes sense. I'll let myself out.</p>



<a name="203037988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203037988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> c-cube <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203037988">(Jul 06 2020 at 20:39)</a>:</h4>
<p>It's also crazy hard to solve!<br>
(edit: SMT 2020 just finished today and the invited talk by P. Rümmer was exactly about that: string solving)</p>



<a name="203039650"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203039650" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203039650">(Jul 06 2020 at 20:55)</a>:</h4>
<p>there was also a talk at pldi recently</p>



<a name="203059519"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203059519" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Eh2406 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203059519">(Jul 07 2020 at 01:32)</a>:</h4>
<p>Links?</p>



<a name="203075775"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/dafny/near/203075775" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/dafny.html#203075775">(Jul 07 2020 at 08:01)</a>:</h4>
<p><span class="user-mention silent" data-user-id="304512">c-cube</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/dafny/near/203037988">said</a>:</p>
<blockquote>
<p>It's also crazy hard to solve!<br>
(edit: SMT 2020 just finished today and the invited talk by P. Rümmer was exactly about that: string solving)</p>
</blockquote>
<p>Philipp Rümmer is my supervisor. :)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>